2021-04-11 05:24:36 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=100ms, Wt=101ms. NTI: Rt=4ms, Wt=4ms at most 74 inferences for useful informations.
% NTI summary: 4 cases unresolved, 0 predicates have been ignored: []

app(A,B,C)terminates_if b(A);b(C).
    % optimal. loops found: [app([A|_],x,[A|_])]. NTI took    0ms,72i,72i
app2(A,B,C,D)terminates_if b(A),b(B);b(D).
    % 3 unresolved: [app2(b,f,f,f),app2(f,b,f,f),app2(f,f,f,f)].
    %  NTI took    0ms, 0i,81i
app2len(A,B,C)terminates_if b(A),b(C).
    % 1 unresolved: [app2len(b,f,f)].
    % loops found: [app2len(s(_),x,_),app2len(s(_),x,y)]. NTI took    0ms,74i,74i
list_lensx(A,B)terminates_if b(A);b(B).
    % optimal. loops found: [list_lensx([_|_],s(_))]. NTI took    0ms,72i,72i

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 13 proofs the 4 inferred conditions:

app(f, f, b).
    % ==> termination proof established
app(b, f, f).
    % ==> termination proof established
app(f, b, f).
    % ==> no proof found
app2(f, f, f, b).
    % ==> termination proof established
app2(b, b, f, f).
    % ==> termination proof established
app2(b, f, b, f).
    % ==> no proof found
app2(f, b, b, f).
    % ==> no proof found
app2len(b, f, b).
    % ==> termination proof established
app2len(b, b, f).
    % ==> no proof found
app2len(f, b, b).
    % ==> no proof found
list_lensx(f, b).
    % ==> termination proof established
list_lensx(b, f).
    % ==> termination proof established
list_lensx(f, f).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Tooltip: Editing larger programs in the textarea is cumbersome. Consider using cTI within Emacs or specifying an URL!

Analyzed program:

app2(A,B,Bs,Cs) :-
	app([A,B], Bs, Cs).

app([], As, As).
app([E|Es], Fs, [E|Gs]) :-
 	app(Es, Fs, Gs).

list_lensx([], 0).
list_lensx([_|Xs], s(N)) :-
	list_lensx(Xs, N).

app2len(N, Bs,Cs) :-
	list_lensx(As, N),
	app(As, Bs, Cs).